Step of Proof: eq_atom_eq_true_elim_sqequal 12,41

Inference at * 1 2 
Iof proof for Lemma eq atom eq true elim sqequal:

.....wf..... NILNIL

1. x : Atom
2. y : Atom
  (x =a y ~ tt)  Type 
latex

 by MemCD 
latex


 1: .....subterm..... T:t1:n

 1:   x =a y ~ x =a y
 2: .....subterm..... T:t2:n

 2:   tt ~ tt
 .


Definitionst  T
Lemmasatom sq

origin